COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	%elepha.sli[e89,jmc][e89,jmc]	Elephant 2000 airline program
C00003 00003	\centerline{ELEPHANT 2000 AIRLINE RESERVATION PROGRAM}
C00005 ENDMK
C⊗;
%elepha.sli[e89,jmc][e89,jmc]	Elephant 2000 airline program
\input slide2.tex[1,jmc]
\bigskip
\bigskip
% suppresses vertical bars
\overfullrule=0pt
\centerline{ELEPHANT 2000 AIRLINE RESERVATION PROGRAM}
\bigskip
$${\bf if} ¬full flt {\bf then} accept.request commit admit(psgr,flt)$$
%
$$answer.query committed admit(psgr,flt)$$
%
$$accept.request decommit admit(psgr,flt)$$
%
$$\eqalign{if now = time {\bf then} flt& ∧ committed admit(psgr,flt)\cr
&{\bf then} accept.request admit(psgr,flt)\cr}$$
%
$$full flt ≡ card\{psgr | committed admit(psgr,flt)\} = capacity flt$$
\vfill\eject
\centerline{ELEPHANT 2000 AIRLINE RESERVATION PROGRAM}
\bigskip
$${\bf if} ¬full flt {\bf then accept.request make commitment} admit(psgr,flt)$$
%
$${\bf answer.query exists commitment} admit(psgr,flt)$$
%
$${\bf accept.request cancel commitment} admit(psgr,flt)$$
%
$$\eqalign{{\bf if}& {\bf now = time} flt\cr
& ∧ {\bf exists commitment} admit(psgr,flt)\cr
& ∧ ¬full1 flt\cr
&\quad {\bf then accept.request} admit(psgr,flt)\cr}$$
%
$$\eqalign{full& flt ≡ \cr
&card\{psgr | {\bf exists commitment} admit(psgr,flt)\} = capacity flt\cr}$$
%
$$\eqalign{full1& flt ≡ \cr
&card\{psgr | {\bf did} admit(psgr,flt)\} = capacity flt\cr}$$
\vfill\end